Search Results

Documents authored by Condotta, Jean-François

Document
DOI: 10.4230/LIPIcs.TIME.2021.16
A One-Pass Tree-Shaped Tableau for Defeasible LTL

Authors: Anasse Chafik, Fahima Cheikh-Alili, Jean-François Condotta, and Ivan Varzinczak

Published in: LIPIcs, Volume 206, 28th International Symposium on Temporal Representation and Reasoning (TIME 2021)

Abstract
Defeasible Linear Temporal Logic is a defeasible temporal formalism for representing and verifying exception-tolerant systems. It is based on Linear Temporal Logic (LTL) and builds on the preferential approach of Kraus et al. for non-monotonic reasoning, which allows us to formalize and reason with exceptions. In this paper, we tackle the satisfiability checking problem for defeasible LTL. One of the methods for satisfiability checking in LTL is the one-pass tree shaped analytic tableau proposed by Reynolds. We adapt his tableau to defeasible LTL by integrating the preferential semantics to the method. The novelty of this work is in showing how the preferential semantics works in a tableau method for defeasible linear temporal logic. We introduce a sound and complete tableau method for a fragment that can serve as the basis for further exploring tableau methods for this logic.
Cite as

Anasse Chafik, Fahima Cheikh-Alili, Jean-François Condotta, and Ivan Varzinczak. A One-Pass Tree-Shaped Tableau for Defeasible LTL. In 28th International Symposium on Temporal Representation and Reasoning (TIME 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 206, pp. 16:1-16:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{chafik_et_al:LIPIcs.TIME.2021.16,
  author =	{Chafik, Anasse and Cheikh-Alili, Fahima and Condotta, Jean-Fran\c{c}ois and Varzinczak, Ivan},
  title =	{{A One-Pass Tree-Shaped Tableau for Defeasible LTL}},
  booktitle =	{28th International Symposium on Temporal Representation and Reasoning (TIME 2021)},
  pages =	{16:1--16:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-206-8},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{206},
  editor =	{Combi, Carlo and Eder, Johann and Reynolds, Mark},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2021.16},
  URN =		{urn:nbn:de:0030-drops-147924},
  doi =		{10.4230/LIPIcs.TIME.2021.16},
  annote =	{Keywords: Temporal logic, Non-monotonic reasoning, Tableau Calculi}
}
Document
DOI: 10.4230/LIPIcs.TIME.2020.19
On the Decidability of a Fragment of preferential LTL

Authors: Anasse Chafik, Fahima Cheikh-Alili, Jean-François Condotta, and Ivan Varzinczak

Published in: LIPIcs, Volume 178, 27th International Symposium on Temporal Representation and Reasoning (TIME 2020)

Abstract
Linear Temporal Logic (LTL) has found extensive applications in Computer Science and Artificial Intelligence, notably as a formal framework for representing and verifying computer systems that vary over time. Non-monotonic reasoning, on the other hand, allows us to formalize and reason with exceptions and the dynamics of information. The goal of this paper is therefore to enrich temporal formalisms with non-monotonic reasoning features. We do so by investigating a preferential semantics for defeasible LTL along the lines of that extensively studied by Kraus et al. in the propositional case and recently extended to modal and description logics. The main contribution of the paper is a decidability result for a meaningful fragment of preferential LTL that can serve as the basis for further exploration of defeasibility in temporal formalisms.
Cite as

Anasse Chafik, Fahima Cheikh-Alili, Jean-François Condotta, and Ivan Varzinczak. On the Decidability of a Fragment of preferential LTL. In 27th International Symposium on Temporal Representation and Reasoning (TIME 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 178, pp. 19:1-19:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{chafik_et_al:LIPIcs.TIME.2020.19,
  author =	{Chafik, Anasse and Cheikh-Alili, Fahima and Condotta, Jean-Fran\c{c}ois and Varzinczak, Ivan},
  title =	{{On the Decidability of a Fragment of preferential LTL}},
  booktitle =	{27th International Symposium on Temporal Representation and Reasoning (TIME 2020)},
  pages =	{19:1--19:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-167-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{178},
  editor =	{Mu\~{n}oz-Velasco, Emilio and Ozaki, Ana and Theobald, Martin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2020.19},
  URN =		{urn:nbn:de:0030-drops-129871},
  doi =		{10.4230/LIPIcs.TIME.2020.19},
  annote =	{Keywords: Knowledge Representation, non-monotonic reasoning, temporal logic}
}
Document
DOI: 10.4230/LIPIcs.TIME.2017.19
Collective Singleton-Based Consistency for Qualitative Constraint Networks

Authors: Michael Sioutis, Anastasia Paparrizou, and Jean-François Condotta

Published in: LIPIcs, Volume 90, 24th International Symposium on Temporal Representation and Reasoning (TIME 2017)

Abstract
Partial singleton closure under weak composition, or partial singleton (weak) path-consistency for short, is essential for approximating satisfiability of qualitative constraints networks. Briefly put, partial singleton path-consistency ensures that each base relation of each of the constraints of a qualitative constraint network can define a singleton relation in the corresponding partial closure of that network under weak composition, or in its corresponding partially (weak) path-consistent subnetwork for short. In particular, partial singleton path-consistency has been shown to play a crucial role in tackling the minimal labeling problem of a qualitative constraint network, which is the problem of finding the strongest implied constraints of that network. In this paper, we propose a stronger local consistency that couples partial singleton path-consistency with the idea of collectively deleting certain unfeasible base relations by exploiting singleton checks. We then propose an efficient algorithm for enforcing this consistency that, given a qualitative constraint network, performs fewer constraint checks than the respective algorithm for enforcing partial singleton path-consistency in that network. We formally prove certain properties of our new local consistency, and motivate its usefulness through demonstrative examples and a preliminary experimental evaluation with qualitative constraint networks of Interval Algebra.
Cite as

Michael Sioutis, Anastasia Paparrizou, and Jean-François Condotta. Collective Singleton-Based Consistency for Qualitative Constraint Networks. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 19:1-19:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{sioutis_et_al:LIPIcs.TIME.2017.19,
  author =	{Sioutis, Michael and Paparrizou, Anastasia and Condotta, Jean-Fran\c{c}ois},
  title =	{{Collective Singleton-Based Consistency for Qualitative Constraint Networks}},
  booktitle =	{24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
  pages =	{19:1--19:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-052-1},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{90},
  editor =	{Schewe, Sven and Schneider, Thomas and Wijsen, Jef},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.19},
  URN =		{urn:nbn:de:0030-drops-79237},
  doi =		{10.4230/LIPIcs.TIME.2017.19},
  annote =	{Keywords: Qualitative constraint network, qualitative spatial and temporal reasoning, partial singleton path-consistency, local consistency, minimal labeling pr}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact